Let's remember where we were with our tableau method for statements.

We defined the concept of flat tableau, where rules were written. I won't write them all down, like this one.

We defined a negative conjunction in our tableau. A tableau is a set of formulas that require conclusive properties.

There is also a set of formulas that require a clash of two things.

First, we require that the case sum is not in T. Second, we require that if not A is in T, then A is not in T.

It doesn't matter how I write it. It shouldn't be A and not A in T.

As announced, we want to draw up a tree-shaped tableau.

We continue to work with quantities of formulas.

We write them in gamma, delta and so on.

We also say that they are final. We call them sequences.

Sequence is always overloaded. In particular, it comes from calculations where I want to show that formulas are valid, while tableau is there to show that formulas are feasible.

In a precise sense, formulas are dual to each other, which is not surprising, because the number of formulas is dual to validity.

I don't think that these are tableau sequences when I want to distinguish them from other sequences.

I generally write these quantities without quantities. In this case, this is the same as gamma unites one quantity of phi and so on.

I write these quantities as quantities, but they are separate lists without swelled brackets.

These things form the nodes of a tree.

Let's start with the case of which I will throw out the phrase and imagine that I code it as A and not A.

I have not done this before, because I want to allow the case that there are no atoms.

We only need to take care of the rules and the conjugation, negation and atom formation of possible clashes.

In this case, we only need to take care of a clash rule.

I could be forced to enter A and not A at the same time.

The rules are almost correct.

The rules are rules for tree knots.

Here is an example where the 350 steps or eight DBA's are here.

Okay, maybe we recognize again, that corresponds to this rule here.

If there was a conjunction in the flat table, I had asked that both conjuncts are in the flat table.

The technical difference is that I throw away the conjunction in the transition from top to bottom.

I only keep the two conjuncts above.

That has its ups and downs.

An up is when the thing shrinks.

If I don't count the commas, then this thing is smaller than this one.

That wouldn't be the case if I just add the two conjuncts.

I get easier induction proofs because my sequences get smaller and smaller.

The downside of this is that I don't see the conjunction anymore.

If I want to know more about complicated formulas, I have to look for the tree.

We'll do that in detail later.

So, let's start with the double negation rule.

I could have a double negation somewhere in my table.

I'll just throw it out.

I'll just remove the double negation.

Then there's the non-and rule.

It's the one that corresponds to the left-hand rule.

I could have a negative conjunction in my sequence.

I have two options to blow up the tree.

Either I say I don't add a negative conjunction.

Or I just throw out the original rule.

Or I just add a negative conjunction.

These are alternative expansion possibilities.

It's not deterministic.

It's obvious that the construction can't be deterministic because it's a problem of NP.